(declare-const v0 Bool)
(declare-const v2 Bool)
(declare-const v4 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const r0 Real)
(declare-const r1 Real)
(declare-const v28 Bool)
(declare-const v32 Bool)
(declare-const r10 Real)
(assert (or (= r1 11838649.53 (* (+ r0 0.6286771 11838649.53 r0) 11838649.53 r0 90199310.0 0.6286771) 90199310.0 90199310.0) v16))
(assert (or (= r1 11838649.53 (* (+ r0 0.6286771 11838649.53 r0) 11838649.53 r0 90199310.0 0.6286771) 90199310.0 90199310.0) v32 v32))
(assert (or v28 (= r1 11838649.53 (* (+ r0 0.6286771 11838649.53 r0) 11838649.53 r0 90199310.0 0.6286771) 90199310.0 90199310.0)))
(check-sat)
(check-sat)
